$\forall$${\it es}$:ES, $e_{1}$, $e_{2}$:E, $P$:(\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id \& ($\neg$($\uparrow$first($e$)))\} $\rightarrow\mathbb{P}$).
\\[0ex](loc($e_{2}$) = loc($e_{1}$) $\in$ Id)
\\[0ex]$\Rightarrow$ $\forall$$e$@loc($e_{1}$). ($\neg$($\uparrow$first($e$))) $\Rightarrow$ Dec($P$($e$))
\\[0ex]$\Rightarrow$ Dec($\exists$$e$$\in$($e_{1}$,$e_{2}$].$P$($e$))